\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$($\mathbb{N}\rightarrow$(IdLnk+Id)+Unit)), $v$:($i$:Id$\rightarrow$M($i$).state),\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow$M($i$).state$\rightarrow$(M($i$).da(locl($a$))+Unit)), $l$:IdLnk, ${\it t'}$:$\mathbb{N}$.
\-\\[0ex]Feasible($D$) $\Rightarrow$ queue($l$;${\it t'}$) $=$ queue($l$;${\it t'}$) $\in$ Msg($\lambda$$l$,${\it tg}$. M(source($l$)).dout2($l$;${\it tg}$)) List
\end{tabbing}